0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 87 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 46 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 183 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 31 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPOrderProof (⇔, 37 ms)
↳36 QDP
↳37 DependencyGraphProof (⇔, 0 ms)
↳38 TRUE
↳39 PiDP
↳40 UsableRulesProof (⇔, 0 ms)
↳41 PiDP
↳42 PiDPToQDPProof (⇒, 0 ms)
↳43 QDP
↳44 QDPSizeChangeProof (⇔, 0 ms)
↳45 YES
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
REMD_IN_GAG(T7, s(T16), T9) → U4_GAG(T7, T16, T9, subC_in_gaa(T7, T16, X7))
REMD_IN_GAG(T7, s(T16), T9) → SUBC_IN_GAA(T7, T16, X7)
SUBC_IN_GAA(s(T31), T33, X40) → U3_GAA(T31, T33, X40, subA_in_gaa(T31, T33, X40))
SUBC_IN_GAA(s(T31), T33, X40) → SUBA_IN_GAA(T31, T33, X40)
SUBA_IN_GAA(s(T44), s(T46), X64) → U1_GAA(T44, T46, X64, subA_in_gaa(T44, T46, X64))
SUBA_IN_GAA(s(T44), s(T46), X64) → SUBA_IN_GAA(T44, T46, X64)
REMD_IN_GAG(T7, s(T20), T9) → U5_GAG(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_GAG(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_GAG(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
U5_GAG(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → REMD_IN_GGG(T19, s(T20), T9)
REMD_IN_GGG(T7, s(T16), T9) → U4_GGG(T7, T16, T9, subC_in_gga(T7, T16, X7))
REMD_IN_GGG(T7, s(T16), T9) → SUBC_IN_GGA(T7, T16, X7)
SUBC_IN_GGA(s(T31), T33, X40) → U3_GGA(T31, T33, X40, subA_in_gga(T31, T33, X40))
SUBC_IN_GGA(s(T31), T33, X40) → SUBA_IN_GGA(T31, T33, X40)
SUBA_IN_GGA(s(T44), s(T46), X64) → U1_GGA(T44, T46, X64, subA_in_gga(T44, T46, X64))
SUBA_IN_GGA(s(T44), s(T46), X64) → SUBA_IN_GGA(T44, T46, X64)
REMD_IN_GGG(T7, s(T20), T9) → U5_GGG(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_GGG(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_GGG(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
U5_GGG(T7, T20, T9, subC_out_gga(T7, T20, T19)) → REMD_IN_GGG(T19, s(T20), T9)
REMD_IN_GGG(s(T79), s(T81), s(T79)) → U7_GGG(T79, T81, geqB_in_gg(T79, T81))
REMD_IN_GGG(s(T79), s(T81), s(T79)) → GEQB_IN_GG(T79, T81)
GEQB_IN_GG(s(T92), s(T94)) → U2_GG(T92, T94, geqB_in_gg(T92, T94))
GEQB_IN_GG(s(T92), s(T94)) → GEQB_IN_GG(T92, T94)
REMD_IN_GAG(s(T79), s(T81), s(T79)) → U7_GAG(T79, T81, geqB_in_ga(T79, T81))
REMD_IN_GAG(s(T79), s(T81), s(T79)) → GEQB_IN_GA(T79, T81)
GEQB_IN_GA(s(T92), s(T94)) → U2_GA(T92, T94, geqB_in_ga(T92, T94))
GEQB_IN_GA(s(T92), s(T94)) → GEQB_IN_GA(T92, T94)
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
REMD_IN_GAG(T7, s(T16), T9) → U4_GAG(T7, T16, T9, subC_in_gaa(T7, T16, X7))
REMD_IN_GAG(T7, s(T16), T9) → SUBC_IN_GAA(T7, T16, X7)
SUBC_IN_GAA(s(T31), T33, X40) → U3_GAA(T31, T33, X40, subA_in_gaa(T31, T33, X40))
SUBC_IN_GAA(s(T31), T33, X40) → SUBA_IN_GAA(T31, T33, X40)
SUBA_IN_GAA(s(T44), s(T46), X64) → U1_GAA(T44, T46, X64, subA_in_gaa(T44, T46, X64))
SUBA_IN_GAA(s(T44), s(T46), X64) → SUBA_IN_GAA(T44, T46, X64)
REMD_IN_GAG(T7, s(T20), T9) → U5_GAG(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_GAG(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_GAG(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
U5_GAG(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → REMD_IN_GGG(T19, s(T20), T9)
REMD_IN_GGG(T7, s(T16), T9) → U4_GGG(T7, T16, T9, subC_in_gga(T7, T16, X7))
REMD_IN_GGG(T7, s(T16), T9) → SUBC_IN_GGA(T7, T16, X7)
SUBC_IN_GGA(s(T31), T33, X40) → U3_GGA(T31, T33, X40, subA_in_gga(T31, T33, X40))
SUBC_IN_GGA(s(T31), T33, X40) → SUBA_IN_GGA(T31, T33, X40)
SUBA_IN_GGA(s(T44), s(T46), X64) → U1_GGA(T44, T46, X64, subA_in_gga(T44, T46, X64))
SUBA_IN_GGA(s(T44), s(T46), X64) → SUBA_IN_GGA(T44, T46, X64)
REMD_IN_GGG(T7, s(T20), T9) → U5_GGG(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_GGG(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_GGG(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
U5_GGG(T7, T20, T9, subC_out_gga(T7, T20, T19)) → REMD_IN_GGG(T19, s(T20), T9)
REMD_IN_GGG(s(T79), s(T81), s(T79)) → U7_GGG(T79, T81, geqB_in_gg(T79, T81))
REMD_IN_GGG(s(T79), s(T81), s(T79)) → GEQB_IN_GG(T79, T81)
GEQB_IN_GG(s(T92), s(T94)) → U2_GG(T92, T94, geqB_in_gg(T92, T94))
GEQB_IN_GG(s(T92), s(T94)) → GEQB_IN_GG(T92, T94)
REMD_IN_GAG(s(T79), s(T81), s(T79)) → U7_GAG(T79, T81, geqB_in_ga(T79, T81))
REMD_IN_GAG(s(T79), s(T81), s(T79)) → GEQB_IN_GA(T79, T81)
GEQB_IN_GA(s(T92), s(T94)) → U2_GA(T92, T94, geqB_in_ga(T92, T94))
GEQB_IN_GA(s(T92), s(T94)) → GEQB_IN_GA(T92, T94)
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
GEQB_IN_GA(s(T92), s(T94)) → GEQB_IN_GA(T92, T94)
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
GEQB_IN_GA(s(T92), s(T94)) → GEQB_IN_GA(T92, T94)
GEQB_IN_GA(s(T92)) → GEQB_IN_GA(T92)
From the DPs we obtained the following set of size-change graphs:
GEQB_IN_GG(s(T92), s(T94)) → GEQB_IN_GG(T92, T94)
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
GEQB_IN_GG(s(T92), s(T94)) → GEQB_IN_GG(T92, T94)
GEQB_IN_GG(s(T92), s(T94)) → GEQB_IN_GG(T92, T94)
From the DPs we obtained the following set of size-change graphs:
SUBA_IN_GGA(s(T44), s(T46), X64) → SUBA_IN_GGA(T44, T46, X64)
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
SUBA_IN_GGA(s(T44), s(T46), X64) → SUBA_IN_GGA(T44, T46, X64)
SUBA_IN_GGA(s(T44), s(T46)) → SUBA_IN_GGA(T44, T46)
From the DPs we obtained the following set of size-change graphs:
REMD_IN_GGG(T7, s(T20), T9) → U5_GGG(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_GGG(T7, T20, T9, subC_out_gga(T7, T20, T19)) → REMD_IN_GGG(T19, s(T20), T9)
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
REMD_IN_GGG(T7, s(T20), T9) → U5_GGG(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_GGG(T7, T20, T9, subC_out_gga(T7, T20, T19)) → REMD_IN_GGG(T19, s(T20), T9)
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
REMD_IN_GGG(T7, s(T20), T9) → U5_GGG(T20, T9, subC_in_gga(T7, T20))
U5_GGG(T20, T9, subC_out_gga(T19)) → REMD_IN_GGG(T19, s(T20), T9)
subC_in_gga(s(T31), T33) → U3_gga(subA_in_gga(T31, T33))
U3_gga(subA_out_gga(X40)) → subC_out_gga(X40)
subA_in_gga(s(T44), s(T46)) → U1_gga(subA_in_gga(T44, T46))
subA_in_gga(T51, 0) → subA_out_gga(T51)
U1_gga(subA_out_gga(X64)) → subA_out_gga(X64)
subC_in_gga(x0, x1)
U3_gga(x0)
subA_in_gga(x0, x1)
U1_gga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U5_GGG(T20, T9, subC_out_gga(T19)) → REMD_IN_GGG(T19, s(T20), T9)
POL(0) = 0
POL(REMD_IN_GGG(x1, x2, x3)) = 1 + x1
POL(U1_gga(x1)) = x1
POL(U3_gga(x1)) = x1
POL(U5_GGG(x1, x2, x3)) = 1 + x3
POL(s(x1)) = 1 + x1
POL(subA_in_gga(x1, x2)) = 1 + x1
POL(subA_out_gga(x1)) = 1 + x1
POL(subC_in_gga(x1, x2)) = x1
POL(subC_out_gga(x1)) = 1 + x1
subC_in_gga(s(T31), T33) → U3_gga(subA_in_gga(T31, T33))
subA_in_gga(s(T44), s(T46)) → U1_gga(subA_in_gga(T44, T46))
subA_in_gga(T51, 0) → subA_out_gga(T51)
U3_gga(subA_out_gga(X40)) → subC_out_gga(X40)
U1_gga(subA_out_gga(X64)) → subA_out_gga(X64)
REMD_IN_GGG(T7, s(T20), T9) → U5_GGG(T20, T9, subC_in_gga(T7, T20))
subC_in_gga(s(T31), T33) → U3_gga(subA_in_gga(T31, T33))
U3_gga(subA_out_gga(X40)) → subC_out_gga(X40)
subA_in_gga(s(T44), s(T46)) → U1_gga(subA_in_gga(T44, T46))
subA_in_gga(T51, 0) → subA_out_gga(T51)
U1_gga(subA_out_gga(X64)) → subA_out_gga(X64)
subC_in_gga(x0, x1)
U3_gga(x0)
subA_in_gga(x0, x1)
U1_gga(x0)
SUBA_IN_GAA(s(T44), s(T46), X64) → SUBA_IN_GAA(T44, T46, X64)
remD_in_gag(T7, s(T16), T9) → U4_gag(T7, T16, T9, subC_in_gaa(T7, T16, X7))
subC_in_gaa(s(T31), T33, X40) → U3_gaa(T31, T33, X40, subA_in_gaa(T31, T33, X40))
subA_in_gaa(s(T44), s(T46), X64) → U1_gaa(T44, T46, X64, subA_in_gaa(T44, T46, X64))
subA_in_gaa(T51, 0, T51) → subA_out_gaa(T51, 0, T51)
U1_gaa(T44, T46, X64, subA_out_gaa(T44, T46, X64)) → subA_out_gaa(s(T44), s(T46), X64)
U3_gaa(T31, T33, X40, subA_out_gaa(T31, T33, X40)) → subC_out_gaa(s(T31), T33, X40)
U4_gag(T7, T16, T9, subC_out_gaa(T7, T16, X7)) → remD_out_gag(T7, s(T16), T9)
remD_in_gag(T7, s(T20), T9) → U5_gag(T7, T20, T9, subC_in_gaa(T7, T20, T19))
U5_gag(T7, T20, T9, subC_out_gaa(T7, T20, T19)) → U6_gag(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(T7, s(T16), T9) → U4_ggg(T7, T16, T9, subC_in_gga(T7, T16, X7))
subC_in_gga(s(T31), T33, X40) → U3_gga(T31, T33, X40, subA_in_gga(T31, T33, X40))
subA_in_gga(s(T44), s(T46), X64) → U1_gga(T44, T46, X64, subA_in_gga(T44, T46, X64))
subA_in_gga(T51, 0, T51) → subA_out_gga(T51, 0, T51)
U1_gga(T44, T46, X64, subA_out_gga(T44, T46, X64)) → subA_out_gga(s(T44), s(T46), X64)
U3_gga(T31, T33, X40, subA_out_gga(T31, T33, X40)) → subC_out_gga(s(T31), T33, X40)
U4_ggg(T7, T16, T9, subC_out_gga(T7, T16, X7)) → remD_out_ggg(T7, s(T16), T9)
remD_in_ggg(T7, s(T20), T9) → U5_ggg(T7, T20, T9, subC_in_gga(T7, T20, T19))
U5_ggg(T7, T20, T9, subC_out_gga(T7, T20, T19)) → U6_ggg(T7, T20, T9, remD_in_ggg(T19, s(T20), T9))
remD_in_ggg(s(T79), s(T81), s(T79)) → U7_ggg(T79, T81, geqB_in_gg(T79, T81))
geqB_in_gg(s(T92), s(T94)) → U2_gg(T92, T94, geqB_in_gg(T92, T94))
geqB_in_gg(T99, 0) → geqB_out_gg(T99, 0)
U2_gg(T92, T94, geqB_out_gg(T92, T94)) → geqB_out_gg(s(T92), s(T94))
U7_ggg(T79, T81, geqB_out_gg(T79, T81)) → remD_out_ggg(s(T79), s(T81), s(T79))
U6_ggg(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_ggg(T7, s(T20), T9)
U6_gag(T7, T20, T9, remD_out_ggg(T19, s(T20), T9)) → remD_out_gag(T7, s(T20), T9)
remD_in_gag(s(T79), s(T81), s(T79)) → U7_gag(T79, T81, geqB_in_ga(T79, T81))
geqB_in_ga(s(T92), s(T94)) → U2_ga(T92, T94, geqB_in_ga(T92, T94))
geqB_in_ga(T99, 0) → geqB_out_ga(T99, 0)
U2_ga(T92, T94, geqB_out_ga(T92, T94)) → geqB_out_ga(s(T92), s(T94))
U7_gag(T79, T81, geqB_out_ga(T79, T81)) → remD_out_gag(s(T79), s(T81), s(T79))
SUBA_IN_GAA(s(T44), s(T46), X64) → SUBA_IN_GAA(T44, T46, X64)
SUBA_IN_GAA(s(T44)) → SUBA_IN_GAA(T44)
From the DPs we obtained the following set of size-change graphs: